\begin{tabbing}
$\forall$${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} , $Q$, $R$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} . Dec($Q$($e$)))
\\[0ex]$\Rightarrow$ \=([$e_{1}$,$e_{2}$]$\sim$([$a$,$b$].$b$ = first $e$ $\geq$ $a$.$Q$($e$) \& $\forall$$e$$\in$[$a$,$b$).$\neg$$R$($e$))+\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ($e_{1}$ $\leq$loc $e_{2}$  \& $Q$($e_{2}$) \& $\forall$$e$$\in$[$e_{1}$,$e_{2}$].$R$($e$) $\Rightarrow$ $Q$($e$)))
\-
\end{tabbing}